A,B:Type, d:EqDecider(B). strong-subtype(A; B)  (d  EqDecider(A)) 

latex

Definitions	s = t, P  Q, P  Q, subtype(S; T), suptype(S; T), , P  Q, prop{i:l}, b, P  Q, EqDecider(T), x:A. B(x), strong-subtype(A; B), A c B, t  T
Lemmas	deq wf, strong-subtype wf, assert wf, iff wf, bool wf, rev implies wf